Nuprl Definition : uni_sat
11,40
postcript
pdf
a
=!
x
:
T
.
Q
(
x
) ==
Q
(
a
) & (
a'
:
T
.
Q
(
a'
)
(
a'
=
a
))
latex
clarification:
a
=!
x
:
T
.
Q
(
x
) ==
Q
(
a
) & (
a'
:
T
.
Q
(
a'
)
(
a'
=
a
T
))
latex
Definitions
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
FDL editor aliases
uni_sat
origin
a':T. Q(a') 
(a' = a))
a':T. Q(a') (a' = a 
T)) a':T. Q(a') (a' = a))
a':T. Q(a') (a' = a T)) x:A. B(x) Q